(1) CpxTrsMatchBoundsProof (EQUIVALENT transformation)
A linear upper bound on the runtime complexity of the TRS R could be shown with a Match Bound [MATCHBOUNDS1,MATCHBOUNDS2] of 2.
The certificate found is represented by the following graph.
Start state: 715
Accept states: [716]
Transitions:
715→716[0_1|0]
715→715[1_1|0, 2_1|0, 3_1|0, 4_1|0, 5_1|0]
715→717[5_1|1]
715→735[5_1|1]
715→759[5_1|1]
717→718[4_1|1]
718→719[3_1|1]
719→720[2_1|1]
720→721[1_1|1]
721→722[0_1|1]
722→723[5_1|1]
723→724[4_1|1]
724→725[3_1|1]
725→726[2_1|1]
726→727[1_1|1]
727→728[0_1|1]
728→729[1_1|1]
729→730[1_1|1]
730→731[5_1|1]
731→732[4_1|1]
732→733[3_1|1]
733→734[2_1|1]
734→716[0_1|1]
734→722[0_1|1]
734→740[0_1|1]
734→764[0_1|1]
735→736[4_1|1]
736→737[3_1|1]
737→738[2_1|1]
738→739[1_1|1]
739→740[0_1|1]
740→741[5_1|1]
741→742[4_1|1]
742→743[3_1|1]
743→744[2_1|1]
744→745[1_1|1]
745→746[0_1|1]
746→747[5_1|1]
747→748[4_1|1]
748→749[3_1|1]
749→750[2_1|1]
750→751[1_1|1]
751→752[0_1|1]
752→753[1_1|1]
753→754[1_1|1]
754→755[5_1|1]
755→756[4_1|1]
756→757[3_1|1]
757→758[2_1|1]
758→716[1_1|1]
758→722[1_1|1]
758→740[1_1|1]
758→764[1_1|1]
758→789[5_1|2]
758→807[5_1|2]
758→831[5_1|2]
759→760[4_1|1]
760→761[3_1|1]
761→762[2_1|1]
762→763[1_1|1]
763→764[0_1|1]
764→765[5_1|1]
765→766[4_1|1]
766→767[3_1|1]
767→768[2_1|1]
768→769[1_1|1]
769→770[0_1|1]
770→771[5_1|1]
771→772[4_1|1]
772→773[3_1|1]
773→774[2_1|1]
774→775[1_1|1]
775→776[0_1|1]
776→777[5_1|1]
777→778[4_1|1]
778→779[3_1|1]
779→780[2_1|1]
780→781[1_1|1]
781→782[0_1|1]
782→783[1_1|1]
783→784[1_1|1]
784→785[5_1|1]
785→786[4_1|1]
786→787[3_1|1]
787→788[2_1|1]
788→716[1_1|1]
788→722[1_1|1]
788→740[1_1|1]
788→764[1_1|1]
788→789[5_1|2]
788→807[5_1|2]
788→831[5_1|2]
789→790[4_1|2]
790→791[3_1|2]
791→792[2_1|2]
792→793[1_1|2]
793→794[0_1|2]
794→795[5_1|2]
795→796[4_1|2]
796→797[3_1|2]
797→798[2_1|2]
798→799[1_1|2]
799→800[0_1|2]
800→801[1_1|2]
801→802[1_1|2]
802→803[5_1|2]
803→804[4_1|2]
804→805[3_1|2]
805→806[2_1|2]
806→728[0_1|2]
806→746[0_1|2]
806→770[0_1|2]
807→808[4_1|2]
808→809[3_1|2]
809→810[2_1|2]
810→811[1_1|2]
811→812[0_1|2]
812→813[5_1|2]
813→814[4_1|2]
814→815[3_1|2]
815→816[2_1|2]
816→817[1_1|2]
817→818[0_1|2]
818→819[5_1|2]
819→820[4_1|2]
820→821[3_1|2]
821→822[2_1|2]
822→823[1_1|2]
823→824[0_1|2]
824→825[1_1|2]
825→826[1_1|2]
826→827[5_1|2]
827→828[4_1|2]
828→829[3_1|2]
829→830[2_1|2]
830→728[1_1|2]
830→746[1_1|2]
830→770[1_1|2]
830→861[5_1|2]
830→879[5_1|2]
830→903[5_1|2]
831→832[4_1|2]
832→833[3_1|2]
833→834[2_1|2]
834→835[1_1|2]
835→836[0_1|2]
836→837[5_1|2]
837→838[4_1|2]
838→839[3_1|2]
839→840[2_1|2]
840→841[1_1|2]
841→842[0_1|2]
842→843[5_1|2]
843→844[4_1|2]
844→845[3_1|2]
845→846[2_1|2]
846→847[1_1|2]
847→848[0_1|2]
848→849[5_1|2]
849→850[4_1|2]
850→851[3_1|2]
851→852[2_1|2]
852→853[1_1|2]
853→854[0_1|2]
854→855[1_1|2]
855→856[1_1|2]
856→857[5_1|2]
857→858[4_1|2]
858→859[3_1|2]
859→860[2_1|2]
860→728[1_1|2]
860→746[1_1|2]
860→770[1_1|2]
860→861[5_1|2]
860→879[5_1|2]
860→903[5_1|2]
861→862[4_1|2]
862→863[3_1|2]
863→864[2_1|2]
864→865[1_1|2]
865→866[0_1|2]
866→867[5_1|2]
867→868[4_1|2]
868→869[3_1|2]
869→870[2_1|2]
870→871[1_1|2]
871→872[0_1|2]
872→873[1_1|2]
873→874[1_1|2]
874→875[5_1|2]
875→876[4_1|2]
876→877[3_1|2]
877→878[2_1|2]
878→752[0_1|2]
878→776[0_1|2]
879→880[4_1|2]
880→881[3_1|2]
881→882[2_1|2]
882→883[1_1|2]
883→884[0_1|2]
884→885[5_1|2]
885→886[4_1|2]
886→887[3_1|2]
887→888[2_1|2]
888→889[1_1|2]
889→890[0_1|2]
890→891[5_1|2]
891→892[4_1|2]
892→893[3_1|2]
893→894[2_1|2]
894→895[1_1|2]
895→896[0_1|2]
896→897[1_1|2]
897→898[1_1|2]
898→899[5_1|2]
899→900[4_1|2]
900→901[3_1|2]
901→902[2_1|2]
902→752[1_1|2]
902→776[1_1|2]
902→933[5_1|2]
902→951[5_1|2]
902→975[5_1|2]
903→904[4_1|2]
904→905[3_1|2]
905→906[2_1|2]
906→907[1_1|2]
907→908[0_1|2]
908→909[5_1|2]
909→910[4_1|2]
910→911[3_1|2]
911→912[2_1|2]
912→913[1_1|2]
913→914[0_1|2]
914→915[5_1|2]
915→916[4_1|2]
916→917[3_1|2]
917→918[2_1|2]
918→919[1_1|2]
919→920[0_1|2]
920→921[5_1|2]
921→922[4_1|2]
922→923[3_1|2]
923→924[2_1|2]
924→925[1_1|2]
925→926[0_1|2]
926→927[1_1|2]
927→928[1_1|2]
928→929[5_1|2]
929→930[4_1|2]
930→931[3_1|2]
931→932[2_1|2]
932→752[1_1|2]
932→776[1_1|2]
932→933[5_1|2]
932→951[5_1|2]
932→975[5_1|2]
933→934[4_1|2]
934→935[3_1|2]
935→936[2_1|2]
936→937[1_1|2]
937→938[0_1|2]
938→939[5_1|2]
939→940[4_1|2]
940→941[3_1|2]
941→942[2_1|2]
942→943[1_1|2]
943→944[0_1|2]
944→945[1_1|2]
945→946[1_1|2]
946→947[5_1|2]
947→948[4_1|2]
948→949[3_1|2]
949→950[2_1|2]
950→782[0_1|2]
951→952[4_1|2]
952→953[3_1|2]
953→954[2_1|2]
954→955[1_1|2]
955→956[0_1|2]
956→957[5_1|2]
957→958[4_1|2]
958→959[3_1|2]
959→960[2_1|2]
960→961[1_1|2]
961→962[0_1|2]
962→963[5_1|2]
963→964[4_1|2]
964→965[3_1|2]
965→966[2_1|2]
966→967[1_1|2]
967→968[0_1|2]
968→969[1_1|2]
969→970[1_1|2]
970→971[5_1|2]
971→972[4_1|2]
972→973[3_1|2]
973→974[2_1|2]
974→782[1_1|2]
975→976[4_1|2]
976→977[3_1|2]
977→978[2_1|2]
978→979[1_1|2]
979→980[0_1|2]
980→981[5_1|2]
981→982[4_1|2]
982→983[3_1|2]
983→984[2_1|2]
984→985[1_1|2]
985→986[0_1|2]
986→987[5_1|2]
987→988[4_1|2]
988→989[3_1|2]
989→990[2_1|2]
990→991[1_1|2]
991→992[0_1|2]
992→993[5_1|2]
993→994[4_1|2]
994→995[3_1|2]
995→996[2_1|2]
996→997[1_1|2]
997→998[0_1|2]
998→999[1_1|2]
999→1000[1_1|2]
1000→1001[5_1|2]
1001→1002[4_1|2]
1002→1003[3_1|2]
1003→1004[2_1|2]
1004→782[1_1|2]